0 Prolog
↳1 PrologToPiTRSProof (⇒, 0 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 18 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 22 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇒, 0 ms)
↳25 QDP
↳26 QDPOrderProof (⇔, 44 ms)
↳27 QDP
↳28 DependencyGraphProof (⇔, 0 ms)
↳29 TRUE
factor_in_ga(.(X, []), X) → factor_out_ga(.(X, []), X)
factor_in_ga(.(X, .(Y, Xs)), T) → U1_ga(X, Y, Xs, T, times_in_gga(X, Y, Z))
times_in_gga(0, X_, 0) → times_out_gga(0, X_, 0)
times_in_gga(s(X), Y, Z) → U3_gga(X, Y, Z, times_in_gga(X, Y, XY))
U3_gga(X, Y, Z, times_out_gga(X, Y, XY)) → U4_gga(X, Y, Z, plus_in_gga(XY, Y, Z))
plus_in_gga(0, X, X) → plus_out_gga(0, X, X)
plus_in_gga(s(X), Y, s(Z)) → U5_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U5_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U4_gga(X, Y, Z, plus_out_gga(XY, Y, Z)) → times_out_gga(s(X), Y, Z)
U1_ga(X, Y, Xs, T, times_out_gga(X, Y, Z)) → U2_ga(X, Y, Xs, T, factor_in_ga(.(Z, Xs), T))
U2_ga(X, Y, Xs, T, factor_out_ga(.(Z, Xs), T)) → factor_out_ga(.(X, .(Y, Xs)), T)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
factor_in_ga(.(X, []), X) → factor_out_ga(.(X, []), X)
factor_in_ga(.(X, .(Y, Xs)), T) → U1_ga(X, Y, Xs, T, times_in_gga(X, Y, Z))
times_in_gga(0, X_, 0) → times_out_gga(0, X_, 0)
times_in_gga(s(X), Y, Z) → U3_gga(X, Y, Z, times_in_gga(X, Y, XY))
U3_gga(X, Y, Z, times_out_gga(X, Y, XY)) → U4_gga(X, Y, Z, plus_in_gga(XY, Y, Z))
plus_in_gga(0, X, X) → plus_out_gga(0, X, X)
plus_in_gga(s(X), Y, s(Z)) → U5_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U5_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U4_gga(X, Y, Z, plus_out_gga(XY, Y, Z)) → times_out_gga(s(X), Y, Z)
U1_ga(X, Y, Xs, T, times_out_gga(X, Y, Z)) → U2_ga(X, Y, Xs, T, factor_in_ga(.(Z, Xs), T))
U2_ga(X, Y, Xs, T, factor_out_ga(.(Z, Xs), T)) → factor_out_ga(.(X, .(Y, Xs)), T)
FACTOR_IN_GA(.(X, .(Y, Xs)), T) → U1_GA(X, Y, Xs, T, times_in_gga(X, Y, Z))
FACTOR_IN_GA(.(X, .(Y, Xs)), T) → TIMES_IN_GGA(X, Y, Z)
TIMES_IN_GGA(s(X), Y, Z) → U3_GGA(X, Y, Z, times_in_gga(X, Y, XY))
TIMES_IN_GGA(s(X), Y, Z) → TIMES_IN_GGA(X, Y, XY)
U3_GGA(X, Y, Z, times_out_gga(X, Y, XY)) → U4_GGA(X, Y, Z, plus_in_gga(XY, Y, Z))
U3_GGA(X, Y, Z, times_out_gga(X, Y, XY)) → PLUS_IN_GGA(XY, Y, Z)
PLUS_IN_GGA(s(X), Y, s(Z)) → U5_GGA(X, Y, Z, plus_in_gga(X, Y, Z))
PLUS_IN_GGA(s(X), Y, s(Z)) → PLUS_IN_GGA(X, Y, Z)
U1_GA(X, Y, Xs, T, times_out_gga(X, Y, Z)) → U2_GA(X, Y, Xs, T, factor_in_ga(.(Z, Xs), T))
U1_GA(X, Y, Xs, T, times_out_gga(X, Y, Z)) → FACTOR_IN_GA(.(Z, Xs), T)
factor_in_ga(.(X, []), X) → factor_out_ga(.(X, []), X)
factor_in_ga(.(X, .(Y, Xs)), T) → U1_ga(X, Y, Xs, T, times_in_gga(X, Y, Z))
times_in_gga(0, X_, 0) → times_out_gga(0, X_, 0)
times_in_gga(s(X), Y, Z) → U3_gga(X, Y, Z, times_in_gga(X, Y, XY))
U3_gga(X, Y, Z, times_out_gga(X, Y, XY)) → U4_gga(X, Y, Z, plus_in_gga(XY, Y, Z))
plus_in_gga(0, X, X) → plus_out_gga(0, X, X)
plus_in_gga(s(X), Y, s(Z)) → U5_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U5_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U4_gga(X, Y, Z, plus_out_gga(XY, Y, Z)) → times_out_gga(s(X), Y, Z)
U1_ga(X, Y, Xs, T, times_out_gga(X, Y, Z)) → U2_ga(X, Y, Xs, T, factor_in_ga(.(Z, Xs), T))
U2_ga(X, Y, Xs, T, factor_out_ga(.(Z, Xs), T)) → factor_out_ga(.(X, .(Y, Xs)), T)
FACTOR_IN_GA(.(X, .(Y, Xs)), T) → U1_GA(X, Y, Xs, T, times_in_gga(X, Y, Z))
FACTOR_IN_GA(.(X, .(Y, Xs)), T) → TIMES_IN_GGA(X, Y, Z)
TIMES_IN_GGA(s(X), Y, Z) → U3_GGA(X, Y, Z, times_in_gga(X, Y, XY))
TIMES_IN_GGA(s(X), Y, Z) → TIMES_IN_GGA(X, Y, XY)
U3_GGA(X, Y, Z, times_out_gga(X, Y, XY)) → U4_GGA(X, Y, Z, plus_in_gga(XY, Y, Z))
U3_GGA(X, Y, Z, times_out_gga(X, Y, XY)) → PLUS_IN_GGA(XY, Y, Z)
PLUS_IN_GGA(s(X), Y, s(Z)) → U5_GGA(X, Y, Z, plus_in_gga(X, Y, Z))
PLUS_IN_GGA(s(X), Y, s(Z)) → PLUS_IN_GGA(X, Y, Z)
U1_GA(X, Y, Xs, T, times_out_gga(X, Y, Z)) → U2_GA(X, Y, Xs, T, factor_in_ga(.(Z, Xs), T))
U1_GA(X, Y, Xs, T, times_out_gga(X, Y, Z)) → FACTOR_IN_GA(.(Z, Xs), T)
factor_in_ga(.(X, []), X) → factor_out_ga(.(X, []), X)
factor_in_ga(.(X, .(Y, Xs)), T) → U1_ga(X, Y, Xs, T, times_in_gga(X, Y, Z))
times_in_gga(0, X_, 0) → times_out_gga(0, X_, 0)
times_in_gga(s(X), Y, Z) → U3_gga(X, Y, Z, times_in_gga(X, Y, XY))
U3_gga(X, Y, Z, times_out_gga(X, Y, XY)) → U4_gga(X, Y, Z, plus_in_gga(XY, Y, Z))
plus_in_gga(0, X, X) → plus_out_gga(0, X, X)
plus_in_gga(s(X), Y, s(Z)) → U5_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U5_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U4_gga(X, Y, Z, plus_out_gga(XY, Y, Z)) → times_out_gga(s(X), Y, Z)
U1_ga(X, Y, Xs, T, times_out_gga(X, Y, Z)) → U2_ga(X, Y, Xs, T, factor_in_ga(.(Z, Xs), T))
U2_ga(X, Y, Xs, T, factor_out_ga(.(Z, Xs), T)) → factor_out_ga(.(X, .(Y, Xs)), T)
PLUS_IN_GGA(s(X), Y, s(Z)) → PLUS_IN_GGA(X, Y, Z)
factor_in_ga(.(X, []), X) → factor_out_ga(.(X, []), X)
factor_in_ga(.(X, .(Y, Xs)), T) → U1_ga(X, Y, Xs, T, times_in_gga(X, Y, Z))
times_in_gga(0, X_, 0) → times_out_gga(0, X_, 0)
times_in_gga(s(X), Y, Z) → U3_gga(X, Y, Z, times_in_gga(X, Y, XY))
U3_gga(X, Y, Z, times_out_gga(X, Y, XY)) → U4_gga(X, Y, Z, plus_in_gga(XY, Y, Z))
plus_in_gga(0, X, X) → plus_out_gga(0, X, X)
plus_in_gga(s(X), Y, s(Z)) → U5_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U5_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U4_gga(X, Y, Z, plus_out_gga(XY, Y, Z)) → times_out_gga(s(X), Y, Z)
U1_ga(X, Y, Xs, T, times_out_gga(X, Y, Z)) → U2_ga(X, Y, Xs, T, factor_in_ga(.(Z, Xs), T))
U2_ga(X, Y, Xs, T, factor_out_ga(.(Z, Xs), T)) → factor_out_ga(.(X, .(Y, Xs)), T)
PLUS_IN_GGA(s(X), Y, s(Z)) → PLUS_IN_GGA(X, Y, Z)
PLUS_IN_GGA(s(X), Y) → PLUS_IN_GGA(X, Y)
From the DPs we obtained the following set of size-change graphs:
TIMES_IN_GGA(s(X), Y, Z) → TIMES_IN_GGA(X, Y, XY)
factor_in_ga(.(X, []), X) → factor_out_ga(.(X, []), X)
factor_in_ga(.(X, .(Y, Xs)), T) → U1_ga(X, Y, Xs, T, times_in_gga(X, Y, Z))
times_in_gga(0, X_, 0) → times_out_gga(0, X_, 0)
times_in_gga(s(X), Y, Z) → U3_gga(X, Y, Z, times_in_gga(X, Y, XY))
U3_gga(X, Y, Z, times_out_gga(X, Y, XY)) → U4_gga(X, Y, Z, plus_in_gga(XY, Y, Z))
plus_in_gga(0, X, X) → plus_out_gga(0, X, X)
plus_in_gga(s(X), Y, s(Z)) → U5_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U5_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U4_gga(X, Y, Z, plus_out_gga(XY, Y, Z)) → times_out_gga(s(X), Y, Z)
U1_ga(X, Y, Xs, T, times_out_gga(X, Y, Z)) → U2_ga(X, Y, Xs, T, factor_in_ga(.(Z, Xs), T))
U2_ga(X, Y, Xs, T, factor_out_ga(.(Z, Xs), T)) → factor_out_ga(.(X, .(Y, Xs)), T)
TIMES_IN_GGA(s(X), Y, Z) → TIMES_IN_GGA(X, Y, XY)
TIMES_IN_GGA(s(X), Y) → TIMES_IN_GGA(X, Y)
From the DPs we obtained the following set of size-change graphs:
U1_GA(X, Y, Xs, T, times_out_gga(X, Y, Z)) → FACTOR_IN_GA(.(Z, Xs), T)
FACTOR_IN_GA(.(X, .(Y, Xs)), T) → U1_GA(X, Y, Xs, T, times_in_gga(X, Y, Z))
factor_in_ga(.(X, []), X) → factor_out_ga(.(X, []), X)
factor_in_ga(.(X, .(Y, Xs)), T) → U1_ga(X, Y, Xs, T, times_in_gga(X, Y, Z))
times_in_gga(0, X_, 0) → times_out_gga(0, X_, 0)
times_in_gga(s(X), Y, Z) → U3_gga(X, Y, Z, times_in_gga(X, Y, XY))
U3_gga(X, Y, Z, times_out_gga(X, Y, XY)) → U4_gga(X, Y, Z, plus_in_gga(XY, Y, Z))
plus_in_gga(0, X, X) → plus_out_gga(0, X, X)
plus_in_gga(s(X), Y, s(Z)) → U5_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U5_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U4_gga(X, Y, Z, plus_out_gga(XY, Y, Z)) → times_out_gga(s(X), Y, Z)
U1_ga(X, Y, Xs, T, times_out_gga(X, Y, Z)) → U2_ga(X, Y, Xs, T, factor_in_ga(.(Z, Xs), T))
U2_ga(X, Y, Xs, T, factor_out_ga(.(Z, Xs), T)) → factor_out_ga(.(X, .(Y, Xs)), T)
U1_GA(X, Y, Xs, T, times_out_gga(X, Y, Z)) → FACTOR_IN_GA(.(Z, Xs), T)
FACTOR_IN_GA(.(X, .(Y, Xs)), T) → U1_GA(X, Y, Xs, T, times_in_gga(X, Y, Z))
times_in_gga(0, X_, 0) → times_out_gga(0, X_, 0)
times_in_gga(s(X), Y, Z) → U3_gga(X, Y, Z, times_in_gga(X, Y, XY))
U3_gga(X, Y, Z, times_out_gga(X, Y, XY)) → U4_gga(X, Y, Z, plus_in_gga(XY, Y, Z))
U4_gga(X, Y, Z, plus_out_gga(XY, Y, Z)) → times_out_gga(s(X), Y, Z)
plus_in_gga(0, X, X) → plus_out_gga(0, X, X)
plus_in_gga(s(X), Y, s(Z)) → U5_gga(X, Y, Z, plus_in_gga(X, Y, Z))
U5_gga(X, Y, Z, plus_out_gga(X, Y, Z)) → plus_out_gga(s(X), Y, s(Z))
U1_GA(Xs, times_out_gga(Z)) → FACTOR_IN_GA(.(Z, Xs))
FACTOR_IN_GA(.(X, .(Y, Xs))) → U1_GA(Xs, times_in_gga(X, Y))
times_in_gga(0, X_) → times_out_gga(0)
times_in_gga(s(X), Y) → U3_gga(Y, times_in_gga(X, Y))
U3_gga(Y, times_out_gga(XY)) → U4_gga(plus_in_gga(XY, Y))
U4_gga(plus_out_gga(Z)) → times_out_gga(Z)
plus_in_gga(0, X) → plus_out_gga(X)
plus_in_gga(s(X), Y) → U5_gga(plus_in_gga(X, Y))
U5_gga(plus_out_gga(Z)) → plus_out_gga(s(Z))
times_in_gga(x0, x1)
U3_gga(x0, x1)
U4_gga(x0)
plus_in_gga(x0, x1)
U5_gga(x0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
FACTOR_IN_GA(.(X, .(Y, Xs))) → U1_GA(Xs, times_in_gga(X, Y))
POL(.(x1, x2)) = 1 + x2
POL(0) = 0
POL(FACTOR_IN_GA(x1)) = x1
POL(U1_GA(x1, x2)) = 1 + x1
POL(U3_gga(x1, x2)) = 0
POL(U4_gga(x1)) = 0
POL(U5_gga(x1)) = x1
POL(plus_in_gga(x1, x2)) = x2
POL(plus_out_gga(x1)) = x1
POL(s(x1)) = 0
POL(times_in_gga(x1, x2)) = 0
POL(times_out_gga(x1)) = 0
U1_GA(Xs, times_out_gga(Z)) → FACTOR_IN_GA(.(Z, Xs))
times_in_gga(0, X_) → times_out_gga(0)
times_in_gga(s(X), Y) → U3_gga(Y, times_in_gga(X, Y))
U3_gga(Y, times_out_gga(XY)) → U4_gga(plus_in_gga(XY, Y))
U4_gga(plus_out_gga(Z)) → times_out_gga(Z)
plus_in_gga(0, X) → plus_out_gga(X)
plus_in_gga(s(X), Y) → U5_gga(plus_in_gga(X, Y))
U5_gga(plus_out_gga(Z)) → plus_out_gga(s(Z))
times_in_gga(x0, x1)
U3_gga(x0, x1)
U4_gga(x0)
plus_in_gga(x0, x1)
U5_gga(x0)